Nuprl Definition : rframe-p
11,40
postcript
pdf
rframe-p(
es
;
i
;
x
;
L
) ==
k
:Knd. (
hasloc(
k
;
i
))
(
(
k
L
))
es-independent(
es
;
i
;
k
;
x
)
latex
clarification:
rframe-p(
es
;
i
;
x
;
L
)
==
k
:Knd. (
hasloc(
k
;
i
))
(
(
k
L
Knd))
es-independent(
es
;
i
;
k
;
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
b
,
hasloc(
k
;
i
)
,
P
Q
,
A
,
(
x
l
)
,
Knd
,
es-independent(
es
;
i
;
k
;
x
)
FDL editor aliases
rframe-p
origin